Definitions

t  T, f(a), x:A. B(x), x:A  B(x), P  Q, EOrderAxioms(E;pred?;info), P  Q, EState(T), Id, rationals, x:AB(x), pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>, s = t, b, A, Unit, void, isect(A; x.B(x)), top, subtype(S; T), left + right, suptype(S; T), first(e), constant_function(f; A; B), kindcase(k; a.f(a); l,t.g(l;t)), Knd, , e < e', qle(r; s), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, IdLnk, x,y. t(x;y), x. t(x), kind(e), sender(e), link(e), rcv?(e), source(l), pred(e), P  Q, x:A. B(x), False, EqDecider(T), event_system{i:l}, Type

Lemmas

event system wf, deq wf, EOrderAxioms wf, strongwellfounded wf, pred! wf, pred wf, Id wf, lsrc wf, rcv? wf, link wf, sender wf, IdLnk wf, kind wf, loc wf, Msg wf, nat wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, EState wf, val-axiom wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf